package dbc.script;

import bsh.EvalError;
import bsh.Interpreter;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
import org.aspectj.lang.JoinPoint;
import org.aspectj.lang.reflect.MethodSignature;

/**
 * Evaluates preconditions and postconditions on methods annotated with @Pre and @Post.
 * Conditions are dynamically evaluated using a script engine.
 */
aspect ContractAspect {

    private Pattern oldRegex;

    public ContractAspect() {
        //TODO: handle properly $old(exp). Currently, no parenthesis is allowed in exp.
        oldRegex = Pattern.compile("\\$old\\(([^\\(\\)]*)\\)");
    }

    /**
     * Returns a new Interpreter, based on the specified JoinPoint. The JoinPoint's target
     * (if there is one) is set in the context of the interpreter with the name "$this".
     * Each parameter of the method catched by the JoinPoint is set in the context of the
     * interpreter with its own name.
     *
     * @param jp  the JoinPoint used to get the method's target and parameters
     * @return a new Interpreter, whose context contains the JoinPoint's target under the
     *         name "$this" and each parameter of the method under its own name
     */
    private Interpreter getInterpreter(JoinPoint jp) {
        Object target = jp.getTarget();
        MethodSignature ms = (MethodSignature)jp.getSignature();
        String[] paramNames = ms.getParameterNames();
        Object[] paramValues = jp.getArgs();
    
        Interpreter interpreter = new Interpreter();
        
        try {
            //set the target
            if(target != null) {
                interpreter.set("$this", target);
            }
            
            //set the method's parameters
            for(int i = 0; i < paramNames.length; i++) {
                interpreter.set(paramNames[i], paramValues[i]);
            }
        } catch(EvalError e) {
            System.out.println(e.getMessage());
        }
        
        return interpreter;
    }
    
    /**
     * Processes the $old(exp) constructs found in the specified condition.
     * Each occurrence of $old(exp) is replaced in the returned condition by $oldn,
     * where n is different for each occurrence, and $oldn is set in the context of
     * the specified interpreter to the result of exp.
     *
     * @param condition    the condition in which $old(exp) are processed
     * @param interpreter  the interpreter used to evaluate and store old values (named $oldn)
     * @return the processed condition, which is the initial condition in which occurrences
     *         of $old(exp) have been replaced by $oldn, with n different for each occurrence
     */
    private String processOld(String condition, Interpreter interpreter) {
        Matcher m = oldRegex.matcher(condition);
        StringBuffer processedCondition = new StringBuffer();
        
        int i = 1;
        while(m.find()) {
            try {
                //evaluate and store old value in $oldi
                interpreter.eval("$old" + i + " = " + m.group(1) + ";");
            } catch(EvalError e) {
                System.out.println(e.getMessage());
            }
            //replace $old(exp) by $oldi
            m.appendReplacement(processedCondition, "\\$old" + i);
            i++;
        }
        m.appendTail(processedCondition);
        
        return processedCondition.toString();
    }
    
    /**
     * Evaluates preconditions. Handles the following special variables:
     *     $this      refers to the object on which the method was called (if the method is not static)
     */
    before(Pre pre): call(@Pre * *(..)) && @annotation(pre) && !within(ContractAspect) {
        Interpreter interpreter = getInterpreter(thisJoinPoint);
        String condition = pre.value();
        
        try {
            //evaluate the condition
            System.out.println("Precondition " + condition + " -> " + interpreter.eval(condition));
        } catch(EvalError e) {
            System.out.println(e.getMessage());
        }
    }
    
    /**
     * Evaluates postconditions. Handles the following special variables:
     *     $this      refers to the object on which the method was called (if the method is not static)
     *     $return    refers to the value returned by the method (if its return type is not void)
     *     $old(exp)  refers to the value of exp just before the method was executed
     */
    Object around(Post post): call(@Post * *(..)) && @annotation(post) && !within(ContractAspect) {
        Interpreter interpreter = getInterpreter(thisJoinPoint);
        String condition = post.value();
        
        //evaluate and store old values
        String processedCondition = processOld(condition, interpreter);
        
        //execute the method
        Object returnValue = proceed(post);
        
        try {
            //set the returned value
            MethodSignature ms = (MethodSignature)thisJoinPoint.getSignature();
            if(ms.getReturnType() != Void.TYPE) {
                interpreter.set("$return", returnValue);
            }
            
            //evaluate the condition
            System.out.println("Postcondition " + condition + " -> " + interpreter.eval(processedCondition));
        } catch(EvalError e) {
            System.out.println(e.getMessage());
        }
        
        return returnValue;
    }
}
